Inference at * 
Iof proof for Lemma le to lt rw:


  i, j:. {(i  j)  (i < (j+1))} 

latex

 by ((Unfold `guard` 0) 
CollapseTHEN (Lemma `le_to_lt`)) 

latex

C.

Definitions	{T}
Lemmas	le to lt